\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, $B$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]$f$:(\=$\cap$$z$:($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top). \+
\\[0ex]\{$e$:E$\mid$ loc($e$) $=$ source($l$) $\in$ Id \& valtype($e$) $\subseteq\rho$ $A$ \}$\rightarrow$($B$+Unit)).
\-\-\\[0ex]state ${\it ds}$$k$:$A$ sends [${\it tg}$, $e$.$f$($e$):$B$] on $l$ $\in$ Prop
\end{tabbing}